Skip to content

Improve proofs for truncation equivalences #1547

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 74 commits into from
Nov 10, 2025
Merged

Improve proofs for truncation equivalences #1547

merged 74 commits into from
Nov 10, 2025

Conversation

@fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Sep 23, 2025 •
edited
Loading

Adds informal proofs for some lemmas about truncation equivalences, and simplifies the formal proofs.

Builds on #1667

@fredrik-bakke
Copy link
Collaborator Author

fredrik-bakke commented Sep 25, 2025

The typechecker is running out of heap memory?

 Checking category-theory.codensity-monads-on-precategories (/home/runner/work/agda-unimath/agda-unimath/master/src/category-theory/codensity-monads-on-precategories.lagda.md).
agda: Heap exhausted;
agda: Current maximum heap size is 6442450944 bytes (6144 MB).
agda: Use `+RTS -M<size>' to increase it.
Command exited with non-zero status 251

https://github.com/UniMath/agda-unimath/actions/runs/18008557550/job/51236792676?pr=1547#step:5:2374

@fredrik-bakke fredrik-bakke marked this pull request as draft September 26, 2025 05:38
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Nov 6, 2025
@fredrik-bakke
Miscellaneous edits from UniMath#1547
0c440fa
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Nov 6, 2025
@fredrik-bakke
More miscellaneous edits from UniMath#1547
92aafbe
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Nov 6, 2025
@fredrik-bakke
More miscellaneous edits from UniMath#1547
34aae22
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Nov 6, 2025
@fredrik-bakke
More miscellaneous edits from UniMath#1547
6fb0d44
fredrik-bakke added a commit that referenced this pull request Nov 6, 2025
@fredrik-bakke
Miscellaneous edits from #1547 (#1667)
73e5178
@fredrik-bakke fredrik-bakke mentioned this pull request Nov 6, 2025
Draft
@fredrik-bakke fredrik-bakke marked this pull request as ready for review November 6, 2025 17:42
@fredrik-bakke fredrik-bakke mentioned this pull request Nov 6, 2025
Merged
@fredrik-bakke fredrik-bakke changed the title Some informal proofs for truncation equivalences Improve proofs for truncation equivalences Nov 7, 2025
@fredrik-bakke
Copy link
Collaborator Author

fredrik-bakke commented Nov 10, 2025 •
edited
Loading

I'm invoking the self-review policy and will merge this PR in a short while, noting that the newer parts of this PR have been split out into separate PRs #1667 #1669 #1668

fredrik-bakke
fredrik-bakke commented Nov 10, 2025
View reviewed changes
Copy link
Collaborator Author

@fredrik-bakke fredrik-bakke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This concludes my self-review.

@fredrik-bakke fredrik-bakke enabled auto-merge (squash) November 10, 2025 14:19
@fredrik-bakke fredrik-bakke merged commit 12fa484 into UniMath:master Nov 10, 2025
3 checks passed
fredrik-bakke added a commit that referenced this pull request Nov 12, 2025
@fredrik-bakke
Subuniverse equivalences and connected maps (#1669)
ffa7c94 
Formalizes `K`-equivalences and `K`-connected maps with respect to an
arbitrary subuniverse `K`.

Builds on #1547.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

foundation

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@fredrik-bakke